x:chain_config(). ccpred?(x)   

latex

Definitions	s = t, t  T, , x:AB(x), x:A. B(x), Id, tt, ff, , x.A(x), x,y. t(x;y), x. t(x), chain_config_ind(x;head;tail;id.pred(id);id,num.succ(id;num)), chain_config(), ccpred?(x), a:A fp B(a), strong-subtype(A;B), P  Q
Lemmas	member wf, chain config wf, chain config ind wf, bool wf, bfalse wf, btrue wf, Id wf, nat wf